The work proposes the use of streamlining in the context of survey inspired decimation algorithms---a main approach alongside stochastic local search---for effciiently finding solutions to large satisfiable random instances of the Boolean satisfiability (SAT) problem. The paper is well-written and easy to follow (although some hasty mistakes remain, see below). The proposed approach is shown to improve the state of the art (to some extent) in algorithms for solving random k-SAT instances, especially by showing that streamlining constraints allow for solving instances that a closer to the sat-unsat phase transition point than previously for different values of k. In terms of motivations, while I do find it of interest to develop algorithmic approach which allow for more efficiently finding solutions to the hardest random k-SAT instances, it would be beneficial if the authors would expand the introduction with more motivations for the work. In terms of contributions, the proposal consists essentially of combining previous proposed ideas to obtain further advances (which is of course ok, but slightly lowers the novelty aspects).

Mixed-integer linear programs (MILPs) are widely used in artificial intelligence and operations research to model complex decision problems like scheduling and routing. Designing such programs however requires both domain and modelling expertise. In this paper, we study the problem of acquiring MILPs from contextual examples, a novel and realistic setting in which examples capture solutions and non-solutions within a specific context. The resulting learning problem involves acquiring continuous parameters -- namely, a cost vector and a feasibility polytope -- but has a distinctly combinatorial flavor. To solve this complex problem, we also contribute MISSLE, an algorithm for learning MILPs from contextual examples. MISSLE uses a variant of stochastic local search that is guided by the gradient of a continuous surrogate loss function. Our empirical evaluation on synthetic data shows that MISSLE acquires better MILPs faster than alternatives based on stochastic local search and gradient descent.

The maximum vertex weight clique problem (MVWCP) is an important generalization of the maximum clique problem (MCP) that has a wide range of real-world applications. In situations where rigorous guarantees regarding the optimality of solutions are not required, MVWCP is usually solved using stochastic local search (SLS) algorithms, which also define the state of the art for solving this problem. However, there is no single SLS algorithm which gives the best performance across all classes of MVWCP instances, and it is challenging to effectively identify the most suitable algorithm for each class of MVWCP instances. In this work, we follow the paradigm of Programming by Optimization (PbO) to develop a new, flexible and highly parametric SLS framework for solving MVWCP, combining, for the first time, a broad range of effective heuristic mechanisms. By automatically configuring this PbO-MWC framework, we achieve substantial advances in the state-of-the-art in solving MVWCP over a broad range of prominent benchmarks, including two derived from real-world applications in transplantation medicine (kidney exchange) and assessment of research excellence.

We observed that Conjunctive Normal Form (CNF) encodings of structured SAT instances often have a set of consecutive clauses defined over a small number of Boolean variables. To exploit the pattern, we propose a transformation of CNF to an alternative representation, Conjunctive Minterm Canonical Form (CMCF). The transformation is a two-step process: CNF clauses are first partitioned into disjoint subsets such that each subset contains CNF clauses with shared Boolean variables. CNF clauses in each subset are then replaced by Minterm Canonical Form (i.e., partial solutions), which is found by enumeration. We show empirically that a simple Stochastic Local Search (SLS) solver based on CMCF can consistently achieve a higher success rate using fewer evaluations than the SLS solver WalkSAT on two representative classes of structured SAT problems.

Simplifying expressions is important to make numerical integration of large expressions from High Energy Physics tractable. To this end, Horner's method can be used. Finding suitable Horner schemes is assumed to be hard, due to the lack of local heuristics. Recently, MCTS was reported to be able to find near optimal schemes. However, several parameters had to be fine-tuned manually. In this work, we investigate the state space properties of Horner schemes and find that the domain is relatively flat and contains only a few local minima. As a result, the Horner space is appropriate to be explored by Stochastic Local Search (SLS), which has only two parameters: the number of iterations (computation time) and the neighborhood structure. We found a suitable neighborhood structure, leaving only the allowed computation time as a parameter. We performed a range of experiments. The results obtained by SLS are similar or better than those obtained by MCTS. Furthermore, we show that SLS obtains the good results at least 10 times faster. Using SLS, we can speed up numerical integration of many real-world large expressions by at least a factor of 24. For High Energy Physics this means that numerical integrations that took weeks can now be done in hours.

Intensification and diversification are the key factors that control the performance of stochastic local search in satisfiability (SAT). Recently, Novelty Walk has become a popular method for improving diversification of the search and so has been integrated in many well-known SAT solvers such as TNM and gNovelty + . In this paper, we introduce new heuristics to improve the effectiveness of Novelty Walk in terms of reducing search stagnation. In particular, we use weights (based on statistical information collected during the search) to focus the diversification phase onto specific areas of interest. With a given probability, we select the most frequently unsatisfied clause instead of a totally random one as Novelty Walk does. Amongst all the variables appearing in the selected clause, we then select the least flipped variable for the next move. Our experimental results show that the new weight-enhanced diversification method significantly improves the performance of gNovelty$^+$ and thus outperforms other local search SAT solvers on a wide range of structured and random satisfiability benchmarks.

Stochastic local search (SLS) is the dominant paradigm for incomplete SAT and MAXSAT solvers. Early studies on small 3SAT instances found that the use of “best improving” moves did not improve search compared to using an arbitrary “first improving” move. Yet SLS algorithms continue to use best improving moves. We revisit this issue by studying very large random and industrial MAXSAT problems. Because locating best improving moves is more expensive than first improving moves, we designed an “approximate best” improving move algorithm and prove that it is as efficient as first improving move SLS. For industrial problems the first local optima found using best improving moves are statistically significantly better than local optima found using first improving moves. However, this advantage reverses as search continues and algorithms must explore equal moves on plateaus. This reversal appears to be associated with critical variables that are in many clauses and that also yield large improving moves.

Rook Jumping Maze design provides a number of good opportunities for experiential learning of AI concepts, including uninformed search, stochastic local search, machine learning, and objective/utility function design. In this paper we will define the maze and present a collection of exercises that allow exploration of several AI topics in the context of an engaging, fun, and unifying task.